------------- MODULE power2liste -------------

EXTENDS Naturals, FiniteSets, Sequences


CONSTANT P, \* taille maximale de la liste = 2^P
         D  \* type des �l�ments

Power2[i\in Nat] ==
 IF (i = 0) THEN 1 ELSE 2 * Power2[i - 1]

\* ensemble des listes de taille born�e par T, d'�l�ments de type D
BoundedSeq(T) == UNION { [ 1..S -> D ] : S \in 0..T }

ETAT == BoundedSeq(Power2[P])


-------------------------------------------
\* A COMPLETER

Vide == << >>

Unit(d) == << d >>

Join(left, right) == left \o right

Split(join) == LET taille == Len(join) IN
				<< SubSeq(join, 1, taille \div 2), SubSeq(join, taille \div 2 + 1, taille) >>

Pick(liste, d) == d = Head(liste)

Occurrence[liste \in ETAT, d \in D] == 
	CASE (liste = Vide) -> 0
	   [] (Head(liste) = d) -> 1 + Occurrence[Tail(liste), d]
	   [] OTHER                 -> Occurrence[Tail(liste), d]

===========================================
